int main() 
 {
    int a = 0xABCDEF;
    printf("%15d", a);
}

